(declare-sort S0 0)

(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const _28-0 (_ BitVec 28))
(declare-const v6 Bool)
(declare-const _21-1 (_ BitVec 21))
(declare-const _29-0 (_ BitVec 29))
(declare-const v7 Bool)
(assert (forall ((q0 Bool) (q1 (_ BitVec 21))) (=> (xor v3 q0 q0 q0 v7 q0 (= _28-0 (bvsmod _28-0 _28-0) _28-0 _28-0 (bvsmod _28-0 _28-0))) (bvult q1 (concat #b01010001110 #b0110111100)))))
(declare-const v8 Bool)
(declare-const _27-0 (_ BitVec 27))
(declare-const v9 Bool)
(declare-const _24-0 (_ BitVec 24))
(declare-const _18-0 (_ BitVec 18))
(declare-const v10 Bool)
(push)
(declare-const v11 Bool)
(declare-const S0-0 S0)
(declare-const v12 Bool)
(push)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(assert (or v14 v14 v15))
(assert (or (=> (not v7) (or v0 v4 v3 (bvule #b01010001110 #b01010001110))) (not (or v6 (= #b0110111100 #b0110111100 #b0110111100 #b0110111100 #b0110111100) v2 v1 v5 v3)) v14))
(assert (or v0 v1 v13))
(assert (or (not v2) v0 (xor v4 (=> (not v7) (or v0 v4 v3 (bvule #b01010001110 #b01010001110))) v10 (and (= _28-0 (bvsmod _28-0 _28-0) _28-0 _28-0 (bvsmod _28-0 _28-0)) v1 v1 v2 (or v0 v4 v3 (bvule #b01010001110 #b01010001110)) v4 v1) (bvule #b01010001110 #b01010001110) v7 (bvule #b01010001110 #b01010001110) (bvule (bvnot #b01010001110) #b01010001110) v3 (= _28-0 (bvsmod _28-0 _28-0) _28-0 _28-0 (bvsmod _28-0 _28-0)) v1)))
(check-sat)
